| Definitions |  x:A. B(x), P   Q, t  T, snds(l;t), map(f;as), upto(n), Y, if b then t else f fi , tt,  , ff, SQType(T), {T}, Top,  , concat(ll), S  T, reduce(f;k;as), rcvs(l;t), suptype(S; T),  x:A. B(x), P & Q, A c B, E,  b, isrcv(l;a),  A, t.1, t.2, p  q, b,   x. t(x), kind(e), act(e), True, P  Q, P Q, time(e), p = q, sender(e), index(e), i  j , ||as||, A  B, t ...$L, False, {i..j },  , Unit, i j < k, x(s), sends(l;e), FairFifo, Dec(P), P  Q, loc(e),  |
| Lemmas | w-snd-rcv, fair-fifo wf, world wf, length wf1, w-snds wf, w-time wf, non neg length, nat wf, int seg wf, w-Msg wf, w-sends wf, IdLnk wf, w-E wf, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, map append sq, upto wf, concat append, map wf, top wf, w-ml wf, le wf, concat-cons, append nil sq, w-a wf, ldst wf, w-action wf, w-isrcvl wf, filter map upto2, filter wf, w-isnull wf, false wf, pi1 wf, Id wf, pi2 wf, w-rcvs wf, isrcv wf, w-kind wf, w-ekind wf, lnk wf, w-sender wf, w-index wf, eq lnk wf, assert-eq-lnk, cand functionality wrt iff, w-eq-E wf, assert-w-eq-E-iff, assert-w-match, length wf nat, mu wf, w-match wf, mu-property, w-match-unique, band wf, eq id wf, lsrc wf, assert of band, and functionality wrt iff, assert-eq-id, decidable equal Id, length nil |
)))